1. Field of the Invention
The invention relates to verification of a design of an integrated circuit (IC). More specifically, the invention relates to a method and an apparatus for formal verification of an IC design that has been retimed, by moving sequential cells across one or more cells of combinational logic.
2. Related Art
Formal verification is well known in the art. See, for example, U.S. Pat. No. 6,336,206 granted to Lockyear on Jan. 1, 2002 and U.S. Pat. No. 6,668,362 granted to McIlwain et al. on Dec. 23, 2003 both of which are incorporated by reference herein in their entirety, as background. Formal verification is normally performed by a computer that has been suitably programmed with software, such as “Formality” available from Synopsys, Inc. and “Conformal” available from Cadence Design Systems, Inc. Such tools are commonly used to check whether two versions of an IC design at different stages of implementation are functionally equivalent to one another. A first version of the IC design, which is known to be functionally correct, is referred to as a reference design. A second version of the IC design, which is verified against the reference, is referred to as an implementation design. The implementation design is typically a gate-level representation that is generated by a logic synthesis tool which receives as its input the first version which is a register transfer level (RTL) description normally represented using a hardware description language such as Verilog/VHDL. Examples of logic synthesis tools are “Design Compiler” available from Synopsys, and “RTLC” available from Cadence.
When the above-described two designs are read into a formal verification tool, they are both divided up into smaller components called logic cones. A logic cone is a set of combinational logic that is bounded by sequential cells (e.g. “registers”), input-output ports of the IC design (called “primary inputs/outputs”), or black boxes. The contents of a black box are not verified (and are typically not known), but signals at the input of the “black-box” are proven to be equivalent by the formal verification tool, while treating the black-box outputs as primary inputs of the IC design. Output pins of logic cones form compare points, which are to be shown as equivalent between the two designs.
After the two designs are read in, the formal verification tool determines which compare points between the reference and implementation designs correspond to each other. The functionality of each matched compare point is then proven or disproven to be equivalent. This is known in the prior art as combinational equivalency checking. During combinational equivalency checking, it is common for the formal verification tool to assume that a black box in the implementation design is same as its counterpart in the reference design. Note that compare point mismatches can occur if black boxes in the reference design do not match those found in the implementation design.
One type of optimization that may be performed by a logic synthesis tool is called “retiming”. In performing retiming, sequential cells are shifted across combinational logic to transfer associated delay from a path with negative slack to a neighboring path with available slack. Moreover, sequential cells that are being moved may be merged or duplicated.
FIGS. 1A and 1B show examples of a gate-level IC design (respectively labeled G1 and G2) prior to and subsequent to forward retiming. FIGS. 1E and 1F show examples of the gate-level IC design (also labeled G1 and G2) prior to and subsequent to backward retiming. As shown in FIGS. 1B and 1F, retiming operations may change the number of sequential cells, and/or the size of logic cones in the two versions of the gate-level IC design. Other combinational optimizations (such as resynthesis) may further be done on the synthesized circuit G2 to result in the synthesized IC design labeled G4 respectively shown in FIGS. 1C and 1G in which the combinational logic within a given logic cone has changed. The just-described changes may result in compare points that are impossible to match between an IC design and its synthesized version(s).
A formal verification tool (such as Formality available from Synopsys, Inc.) performs its own elaboration of RTL design into a gate-level IC design. For example, FIG. 1D illustrates Formality's elaboration of RTL shown in FIG. 1A. In a similar fashion, FIG. 1H illustrates Formality's elaboration of RTL shown in FIG. 1E. Note that FIG. 1A and FIG. 1E are two example designs whereby their corresponding retimed designs shown in FIG. 1B and FIG. 1F illustrate retiming in forward and backward directions respectively. FIGS. 1C and 1G illustrate designs that are derived from the respective retimed designs in FIGS. 1B and 1F, e.g. after re-synthesis and/or clock gating to lower power consumption and/or scan structure insertion for testing, etc. Due to the structural differences between reference and implementation designs as shown in FIGS. 1C and 1D, and in FIGS. 1G and 1H, any combinational equivalency checking by a formal verification tool may not be meaningful.
Specifically, a synthesis tool (such as the above-described Design Compiler) may be used to synthesize a given RTL design into a gate level IC design G1 followed by retiming to generate IC design G2, followed by re-synthesis to generate IC design G3 (not shown in FIGS. 1A-1H) followed by further processing to generate IC design G4. Due to such operations, the number of sequential cells and their next state functions are usually different in netlist G4 (see FIGS. 1C and 1G) when compared to netlist F1 (see FIGS. 1D and 1H) and netlist G1 (see FIGS. 1C and 1G). The netlists F1 and G1 are equivalent and can be shown to be equivalent by a formal verification tool such as Formality available from Synopsys, Inc. The netlist G4 which is a retimed and resynthesized version of G1, on the other hand, cannot be shown to be equivalent to F1 by a combinational equivalency checking tool without additional processing. One such additional processing is described in a paper entitled “Peripheral Retiming Applied to Circuit Verification” by Brian Lockyear, Synopsys Inc, Advanced Technology Group, 19500 NW Gibbs Drive, Beaverton, Oreg. 97006, which is concurrently filed herewith and incorporated by reference herein in its entirety as background.
The netlists G4 and F1 are not combinationally equivalent. They are sequentially equivalent and can be shown to be equivalent by a sequential equivalency tool. Since retiming is one form of sequential optimization, sequential equivalency checking tools can be used to show the equivalence of retimed designs. Although such sequential equivalency checking tools exist, they are not scalable to practical circuit designs. One example of a sequential equivalency checking tool is SLEC sequential equivalence checking software available from Calypto Design Systems, 2933 Bunker Hill Lane, Suite 202, Santa Clara, Calif. 95054.
To the knowledge of the current inventors, prior art methods for equivalency checking of circuits optimized by retiming required structural similarity between the reference and the implementation designs in order to be able to reverse the effects of retiming optimizations and convert the retiming verification problem into combinational equivalency checking domain. One of these methods is described in an article entitled “REVERSE: Efficient Sequential Verification for Retiming” by Maher Mneimneh and Karem Sakallah, published in “International Workshop on Logic and Synthesis” 2003. This article recognizes the existence of a retiming invariant relating the two circuits, and utilizes that invariant in an induction-based verification paradigm.